\begin{tabbing}
$\forall$$A$, $B$:Realizer.
\\[0ex]R{-}Feasible($A$)
\\[0ex]$\Rightarrow$ R{-}Feasible($B$)
\\[0ex]$\Rightarrow$ (\=$\exists$$i$:Id.\+
\\[0ex]($\forall$$j$:Id. R{-}has{-}loc($A$;$j$) $=$ $i$ = $j$ $\in$ $\mathbb{B}$)
\\[0ex]\& \=$\forall$$k$$\in$dom(R{-}da($A$;$i$)). \+
\\[0ex]
\\[0ex]$T$\==R{-}da($A$;$i$)($k$) $\Rightarrow$ \+
\\[0ex]isrcv($k$)
\\[0ex]$\Rightarrow$ \=(source(lnk($k$)) $=$ $i$ $\in$ Id $\Rightarrow$ $T$ $\subseteq\rho$ R{-}da($B$;destination(lnk($k$)))($k$)?Top)\+
\\[0ex]\& (destination(lnk($k$)) $=$ $i$ $\in$ Id $\Rightarrow$ R{-}da($B$;source(lnk($k$)))($k$)?Void $\subseteq\rho$ $T$))
\-\-\-\-\\[0ex]$\Rightarrow$ R{-}icompat($B$;$A$)
\end{tabbing}